using Microsoft.ExtendedReflection.Collections;
using Microsoft.ExtendedReflection.Logging;
using Microsoft.ExtendedReflection.Reasoning.ExecutionNodes;
using Microsoft.ExtendedReflection.Utilities.Safe.Diagnostics;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.Pex.Engine.SearchFrontiers;
using Microsoft.Pex.Framework.Strategies;

namespace Benchmarks
{
    public sealed class SearchFrontierDepthFirstAttribute :
        PexSearchFrontierAttributeBase
    {
        public SearchFrontierDepthFirstAttribute() : base(false) { }

        protected override IPexSearchFrontier CreateFrontier(
            IPexExplorationEngine host,
            IPexBuiltinSearchFrontiers builtinSearchFrontiers)
        {
            return new SearchFrontier();
        }

        class SearchFrontier : IPexSearchFrontier
        {
            class Wrapper
            {
                public readonly IExecutionNode Node;
                public bool Removed;
                public Wrapper(IExecutionNode node)
                {
                    this.Node = node;
                }
            }

            SafeStack<Wrapper> stack = new SafeStack<Wrapper>();
            SafeDictionary<IExecutionNode, Wrapper> nodes = new SafeDictionary<IExecutionNode, Wrapper>();
            int removed;

            public SearchFrontier() { }

            public void Add(IExecutionNode node)
            {
                SafeDebug.Assert((!this.nodes.ContainsKey(node)), "(!this.nodes.ContainsKey(node))");
                Wrapper w = new Wrapper(node);
                this.stack.Push(w);
                this.nodes[node] = w;
            }

            public void Remove(IExecutionNode node, bool used)
            {
                SafeDebug.Assert((this.nodes.ContainsKey(node)), "(this.nodes.ContainsKey(node))");
                this.nodes[node].Removed = true;
                this.nodes.Remove(node);
            }

            public void LocationUpdated(IExecutionNode node)
            {
                SafeDebug.Assert((this.nodes.ContainsKey(node)), "(this.nodes.ContainsKey(node))");
                // ignore, since we don't use location anyway
            }

            public bool Contains(IExecutionNode node)
            {
                return this.nodes.ContainsKey(node);
            }

            public bool TryRemove(out IExecutionNode node)
            {
                while (this.stack.Count > 0)
                {
                    Wrapper w = this.stack.Pop();
                    if (!w.Removed)
                    {
                        node = w.Node;
                        this.nodes.Remove(node);
                        this.removed++;
                        return true;
                    }
                }
                node = null;
                return false;
            }

            public int SkipMany()
            {
                int half = (this.stack.Count + 1) / 2;
                for (int i = 0; i < half; i++)
                    this.stack.Pop();
                return half;
            }

            public bool HasContent
            {
                get { return this.nodes.Count > 0; }
            }

            public bool IsProgressing
            {
                get { return false; }
            }

            public void DumpStatistics(DumpTreeWriter writer, int depth)
            {
                object token = writer.StartNode(this.GetType().Name);
                writer.WriteLine("stack has {0} entries left; {1} nodes are alive; {2} were removed", this.stack.Count, this.nodes.Count, this.removed);
                writer.EndNode(token);
            }
        }
    }
}